section â¹Preliminaries⺠theory Prelim imports "Fresh_Identifiers.Fresh_String" "Bounded_Deducibility_Security.Trivia" begin subsection â¹The basic types⺠(* This version of string is needed for code generation: *) definition "emptyStr = STR ''''" (* The users of the system: *) datatype name = Nam String.literal definition "emptyName â¡ Nam emptyStr" datatype inform = Info String.literal definition "emptyInfo â¡ Info emptyStr" datatype user = Usr name inform fun nameUser where "nameUser (Usr name info) = name" fun infoUser where "infoUser (Usr name info) = info" definition "emptyUser â¡ Usr emptyName emptyInfo" typedecl raw_data code_printing type_constructor raw_data â (Scala) "java.io.File" (* Images (currently, pdf, to be changed): *) datatype img = emptyImg | Imag raw_data (* Visibility outside the current api: either friends-only or public (i.e., exportable outside to the other apis): *) datatype vis = Vsb String.literal (* Accepted values: friend and public *) abbreviation "FriendV â¡ Vsb (STR ''friend'')" (* abbreviation "InternalV â¡ Vsb (STR ''internal'')" *) abbreviation "PublicV â¡ Vsb (STR ''public'')" fun stringOfVis where "stringOfVis (Vsb str) = str" (* A post consists of a string for title, a string for its text, a (possibly empty) image and a visibility specification: *) datatype title = Tit String.literal definition "emptyTitle â¡ Tit emptyStr" datatype "text" = Txt String.literal definition "emptyText â¡ Txt emptyStr" datatype post = Pst title "text" img (* vis *) (* Getters: *) fun titlePost where "titlePost (Pst title text img) = title" fun textPost where "textPost (Pst title text img) = text" fun imgPost where "imgPost (Pst title text img) = img" (* fun visPost where "visPost (Pst title text img vis) = vis" *) (* Setters: *) fun setTitlePost where "setTitlePost (Pst title text img) title' = Pst title' text img" fun setTextPost where "setTextPost(Pst title text img) text' = Pst title text' img" fun setImgPost where "setImgPost (Pst title text img) img' = Pst title text img'" (* fun setVisPost where "setVisPost (Pst title text img vis) vis' = Pst title text img vis'" *) (* *) definition emptyPost :: post where "emptyPost â¡ Pst emptyTitle emptyText emptyImg" (* FriendV" *) (* initially set to the lowest visibility: friend *) lemma titlePost_emptyPost[simp]: "titlePost emptyPost = emptyTitle" and textPost_emptyPost[simp]: "textPost emptyPost = emptyText" and imgPost_emptyPost[simp]: "imgPost emptyPost = emptyImg" (* and visPost_emptyPost[simp]: "visPost emptyPost = FriendV" *) unfolding emptyPost_def by simp_all lemma set_get_post[simp]: "titlePost (setTitlePost ntc title) = title" "titlePost (setTextPost ntc text) = titlePost ntc" "titlePost (setImgPost ntc img) = titlePost ntc" (* "titlePost (setVisPost ntc vis) = titlePost ntc" *) (* *) "textPost (setTitlePost ntc title) = textPost ntc" "textPost (setTextPost ntc text) = text" "textPost (setImgPost ntc img) = textPost ntc" (* "textPost (setVisPost ntc vis) = textPost ntc" *) (* *) "imgPost (setTitlePost ntc title) = imgPost ntc" "imgPost (setTextPost ntc text) = imgPost ntc" "imgPost (setImgPost ntc img) = img" (* "imgPost (setVisPost ntc vis) = imgPost ntc" *) (* *) (* "visPost (setTitlePost ntc title) = visPost ntc" "visPost (setTextPost ntc text) = visPost ntc" "visPost (setImgPost ntc img) = visPost ntc" "visPost (setVisPost ntc vis) = vis" *) (* *) by(cases ntc, auto)+ lemma setTextPost_absorb[simp]: "setTitlePost (setTitlePost pst tit) tit1 = setTitlePost pst tit1" "setTextPost (setTextPost pst txt) txt1 = setTextPost pst txt1" "setImgPost (setImgPost pst img) img1 = setImgPost pst img1" (* "setVisPost (setVisPost pst vis) vis1 = setVisPost pst vis1" *) by (cases pst, auto)+ datatype password = Psw String.literal definition "emptyPass â¡ Psw emptyStr" datatype salt = Slt String.literal definition "emptySalt â¡ Slt emptyStr" (* Information associated to requests for registration: both for users and apis *) datatype requestInfo = ReqInfo String.literal definition "emptyRequestInfo â¡ ReqInfo emptyStr" subsection â¹Identifiers⺠datatype apiID = Aid String.literal datatype userID = Uid String.literal datatype postID = Pid String.literal definition "emptyApiID â¡ Aid emptyStr" definition "emptyUserID â¡ Uid emptyStr" definition "emptyPostID â¡ Pid emptyStr" (* *) fun apiIDAsStr where "apiIDAsStr (Aid str) = str" definition "getFreshApiID apiIDs â¡ Aid (fresh (set (map apiIDAsStr apiIDs)) (STR ''1''))" lemma ApiID_apiIDAsStr[simp]: "Aid (apiIDAsStr apiID) = apiID" by (cases apiID) auto lemma member_apiIDAsStr_iff[simp]: "str â apiIDAsStr ` apiIDs â· Aid str â apiIDs" by (metis ApiID_apiIDAsStr image_iff apiIDAsStr.simps) lemma getFreshApiID: "¬ getFreshApiID apiIDs ââ apiIDs" using fresh_notIn[of "set (map apiIDAsStr apiIDs)"] unfolding getFreshApiID_def by auto (* *) fun userIDAsStr where "userIDAsStr (Uid str) = str" definition "getFreshUserID userIDs â¡ Uid (fresh (set (map userIDAsStr userIDs)) (STR ''2''))" lemma UserID_userIDAsStr[simp]: "Uid (userIDAsStr userID) = userID" by (cases userID) auto lemma member_userIDAsStr_iff[simp]: "str â userIDAsStr ` (set userIDs) â· Uid str ââ userIDs" by (metis UserID_userIDAsStr image_iff userIDAsStr.simps) lemma getFreshUserID: "¬ getFreshUserID userIDs ââ userIDs" using fresh_notIn[of "set (map userIDAsStr userIDs)"] unfolding getFreshUserID_def by auto (* *) fun postIDAsStr where "postIDAsStr (Pid str) = str" definition "getFreshPostID postIDs â¡ Pid (fresh (set (map postIDAsStr postIDs)) (STR ''3''))" lemma PostID_postIDAsStr[simp]: "Pid (postIDAsStr postID) = postID" by (cases postID) auto lemma member_postIDAsStr_iff[simp]: "str â postIDAsStr ` (set postIDs) â· Pid str ââ postIDs" by (metis PostID_postIDAsStr image_iff postIDAsStr.simps) lemma getFreshPostID: "¬ getFreshPostID postIDs ââ postIDs" using fresh_notIn[of "set (map postIDAsStr postIDs)"] unfolding getFreshPostID_def by auto end
section â¹The CoSMeDis single node specification⺠text â¹This is the specification of a CoSMeDis node, as described in Sections II and IV.B of \cite{cosmedis-SandP2017}. NB: What that paper refers to as "nodes" are referred in this formalization as "APIs". A CoSMeDis node extends CoSMed \cite{cosmed-itp2016,cosmed-jar2018,cosmed-AFP} with inter-node communication actions. ⺠theory System_Specification imports Prelim "Bounded_Deducibility_Security.IO_Automaton" begin text â¹An aspect not handled in this specification is the uniqueness of the node IDs. These are assumed to be handled externally as follows: a node ID is an URI, and therefore is unique.⺠declare List.insert[simp] subsection â¹The stateâº